Matches in value-assignements (V): {{numOfValueMatches}}
Matches in edge-description: {{numOfDescriptionMatches}}
Rank |
Scope |
|||
-V- |
{{line.bestrank}}
|
{{line.desc}}
|
| Precondition (initial variable assignment): |
|
{{precondition}} |
| {{fault.rank}}. | {{fault.score}} | Details: | ||||
Current values:
|
||||||
1 | extern int __VERIFIER_nondet_int(); |
2 | |
3 | extern void __assert_fail (const char *__assertion, const char *__file, |
4 | unsigned int __line, const char *__function) |
5 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); |
6 | extern void __assert_perror_fail (int __errnum, const char *__file, |
7 | unsigned int __line, const char *__function) |
8 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); |
9 | extern void __assert (const char *__assertion, const char *__file, int __line) |
10 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); |
11 | |
12 | void reach_error() { ((void) sizeof ((0) ? 1 : 0), __extension__ ({ if (0) ; else __assert_fail ("0", "Problem10.c", 3, __extension__ __PRETTY_FUNCTION__); })); } |
13 | void reach_error_b(){ reach_error(); } |
14 | void reach_error_a(){ reach_error(); } |
15 | void reach_error_0(){ reach_error_a(); } |
16 | void reach_error_1(){ reach_error_a(); } |
17 | void reach_error_2(){ reach_error_a(); } |
18 | void reach_error_3(){ reach_error_a(); } |
19 | void reach_error_4(){ reach_error_b(); } |
20 | void reach_error_5(){ reach_error_a(); } |
21 | void reach_error_6(){ reach_error_b(); } |
22 | void reach_error_7(){ reach_error_a(); } |
23 | void reach_error_8(){ reach_error_a(); } |
24 | void reach_error_9(){ reach_error_a(); } |
25 | void reach_error_10(){ reach_error_a(); } |
26 | void reach_error_11(){ reach_error_a(); } |
27 | void reach_error_12(){ reach_error_a(); } |
28 | void reach_error_13(){ reach_error_a(); } |
29 | void reach_error_14(){ reach_error_a(); } |
30 | void reach_error_15(){ reach_error_a(); } |
31 | void reach_error_16(){ reach_error_a(); } |
32 | void reach_error_17(){ reach_error_a(); } |
33 | void reach_error_18(){ reach_error_b(); } |
34 | void reach_error_19(){ reach_error_a(); } |
35 | void reach_error_20(){ reach_error_a(); } |
36 | void reach_error_21(){ reach_error_a(); } |
37 | void reach_error_22(){ reach_error_a(); } |
38 | void reach_error_23(){ reach_error_b(); } |
39 | void reach_error_24(){ reach_error_a(); } |
40 | void reach_error_25(){ reach_error_a(); } |
41 | void reach_error_26(){ reach_error_a(); } |
42 | void reach_error_27(){ reach_error_b(); } |
43 | void reach_error_28(){ reach_error_a(); } |
44 | void reach_error_29(){ reach_error_a(); } |
45 | void reach_error_30(){ reach_error_a(); } |
46 | void reach_error_31(){ reach_error_b(); } |
47 | void reach_error_32(){ reach_error_a(); } |
48 | void reach_error_33(){ reach_error_a(); } |
49 | void reach_error_34(){ reach_error_a(); } |
50 | void reach_error_35(){ reach_error_a(); } |
51 | void reach_error_36(){ reach_error_a(); } |
52 | void reach_error_37(){ reach_error_a(); } |
53 | void reach_error_38(){ reach_error_b(); } |
54 | void reach_error_39(){ reach_error_a(); } |
55 | void reach_error_40(){ reach_error_a(); } |
56 | void reach_error_41(){ reach_error_a(); } |
57 | void reach_error_42(){ reach_error_a(); } |
58 | void reach_error_43(){ reach_error_a(); } |
59 | void reach_error_44(){ reach_error_a(); } |
60 | void reach_error_45(){ reach_error_a(); } |
61 | void reach_error_46(){ reach_error_a(); } |
62 | void reach_error_47(){ reach_error_a(); } |
63 | void reach_error_48(){ reach_error_a(); } |
64 | void reach_error_49(){ reach_error_a(); } |
65 | void reach_error_50(){ reach_error_a(); } |
66 | void reach_error_51(){ reach_error_a(); } |
67 | void reach_error_52(){ reach_error_a(); } |
68 | void reach_error_53(){ reach_error_a(); } |
69 | void reach_error_54(){ reach_error_a(); } |
70 | void reach_error_55(){ reach_error_a(); } |
71 | void reach_error_56(){ reach_error_a(); } |
72 | void reach_error_57(){ reach_error_a(); } |
73 | void reach_error_58(){ reach_error_b(); } |
74 | void reach_error_59(){ reach_error_a(); } |
75 | void reach_error_60(){ reach_error_a(); } |
76 | void reach_error_61(){ reach_error_a(); } |
77 | void reach_error_62(){ reach_error_a(); } |
78 | void reach_error_63(){ reach_error_a(); } |
79 | void reach_error_64(){ reach_error_b(); } |
80 | void reach_error_65(){ reach_error_b(); } |
81 | void reach_error_66(){ reach_error_a(); } |
82 | void reach_error_67(){ reach_error_a(); } |
83 | void reach_error_68(){ reach_error_a(); } |
84 | void reach_error_69(){ reach_error_b(); } |
85 | void reach_error_70(){ reach_error_a(); } |
86 | void reach_error_71(){ reach_error_a(); } |
87 | void reach_error_72(){ reach_error_a(); } |
88 | void reach_error_73(){ reach_error_b(); } |
89 | void reach_error_74(){ reach_error_a(); } |
90 | void reach_error_75(){ reach_error_a(); } |
91 | void reach_error_76(){ reach_error_a(); } |
92 | void reach_error_77(){ reach_error_a(); } |
93 | void reach_error_78(){ reach_error_a(); } |
94 | void reach_error_79(){ reach_error_a(); } |
95 | void reach_error_80(){ reach_error_a(); } |
96 | void reach_error_81(){ reach_error_a(); } |
97 | void reach_error_82(){ reach_error_a(); } |
98 | void reach_error_83(){ reach_error_a(); } |
99 | void reach_error_84(){ reach_error_a(); } |
100 | void reach_error_85(){ reach_error_a(); } |
101 | void reach_error_86(){ reach_error_a(); } |
102 | void reach_error_87(){ reach_error_a(); } |
103 | void reach_error_88(){ reach_error_b(); } |
104 | void reach_error_89(){ reach_error_a(); } |
105 | void reach_error_90(){ reach_error_a(); } |
106 | void reach_error_91(){ reach_error_a(); } |
107 | void reach_error_92(){ reach_error_b(); } |
108 | void reach_error_93(){ reach_error_a(); } |
109 | void reach_error_94(){ reach_error_a(); } |
110 | void reach_error_95(){ reach_error_a(); } |
111 | void reach_error_96(){ reach_error_a(); } |
112 | void reach_error_97(){ reach_error_a(); } |
113 | void reach_error_98(){ reach_error_a(); } |
114 | void reach_error_99(){ reach_error_a(); } |
115 | |
116 | |
117 | // inputs |
118 | int inputs[] = {5,1,3,2,4}; |
119 | |
120 | void errorCheck(); |
121 | void calculate_output(int); |
122 | void calculate_outputm1(int); |
123 | void calculate_outputm2(int); |
124 | void calculate_outputm3(int); |
125 | void calculate_outputm4(int); |
126 | void calculate_outputm5(int); |
127 | void calculate_outputm6(int); |
128 | void calculate_outputm7(int); |
129 | void calculate_outputm8(int); |
130 | void calculate_outputm9(int); |
131 | void calculate_outputm10(int); |
132 | void calculate_outputm11(int); |
133 | void calculate_outputm12(int); |
134 | void calculate_outputm13(int); |
135 | void calculate_outputm14(int); |
136 | void calculate_outputm15(int); |
137 | void calculate_outputm16(int); |
138 | void calculate_outputm17(int); |
139 | void calculate_outputm18(int); |
140 | void calculate_outputm19(int); |
141 | void calculate_outputm20(int); |
142 | void calculate_outputm21(int); |
143 | void calculate_outputm22(int); |
144 | void calculate_outputm23(int); |
145 | void calculate_outputm24(int); |
146 | void calculate_outputm25(int); |
147 | void calculate_outputm26(int); |
148 | void calculate_outputm27(int); |
149 | void calculate_outputm28(int); |
150 | void calculate_outputm29(int); |
151 | void calculate_outputm30(int); |
152 | void calculate_outputm31(int); |
153 | void calculate_outputm32(int); |
154 | void calculate_outputm33(int); |
155 | void calculate_outputm34(int); |
156 | void calculate_outputm35(int); |
157 | void calculate_outputm36(int); |
158 | void calculate_outputm37(int); |
159 | void calculate_outputm38(int); |
160 | void calculate_outputm39(int); |
161 | void calculate_outputm40(int); |
162 | void calculate_outputm41(int); |
163 | void calculate_outputm42(int); |
164 | void calculate_outputm43(int); |
165 | void calculate_outputm44(int); |
166 | void calculate_outputm45(int); |
167 | void calculate_outputm46(int); |
168 | void calculate_outputm47(int); |
169 | void calculate_outputm48(int); |
170 | void calculate_outputm49(int); |
171 | void calculate_outputm50(int); |
172 | void calculate_outputm51(int); |
173 | void calculate_outputm52(int); |
174 | void calculate_outputm53(int); |
175 | void calculate_outputm54(int); |
176 | void calculate_outputm55(int); |
177 | void calculate_outputm56(int); |
178 | void calculate_outputm57(int); |
179 | void calculate_outputm58(int); |
180 | void calculate_outputm59(int); |
181 | void calculate_outputm60(int); |
182 | void calculate_outputm61(int); |
183 | void calculate_outputm62(int); |
184 | void calculate_outputm63(int); |
185 | void calculate_outputm64(int); |
186 | void calculate_outputm65(int); |
187 | void calculate_outputm66(int); |
188 | void calculate_outputm67(int); |
189 | void calculate_outputm68(int); |
190 | void calculate_outputm69(int); |
191 | void calculate_outputm70(int); |
192 | void calculate_outputm71(int); |
193 | void calculate_outputm72(int); |
194 | void calculate_outputm73(int); |
195 | void calculate_outputm74(int); |
196 | void calculate_outputm75(int); |
197 | void calculate_outputm76(int); |
198 | void calculate_outputm77(int); |
199 | void calculate_outputm78(int); |
200 | void calculate_outputm79(int); |
201 | void calculate_outputm80(int); |
202 | void calculate_outputm81(int); |
203 | void calculate_outputm82(int); |
204 | void calculate_outputm83(int); |
205 | void calculate_outputm84(int); |
206 | void calculate_outputm85(int); |
207 | void calculate_outputm86(int); |
208 | void calculate_outputm87(int); |
209 | void calculate_outputm88(int); |
210 | void calculate_outputm89(int); |
211 | void calculate_outputm90(int); |
212 | void calculate_outputm91(int); |
213 | void calculate_outputm92(int); |
214 | void calculate_outputm93(int); |
215 | void calculate_outputm94(int); |
216 | void calculate_outputm95(int); |
217 | void calculate_outputm96(int); |
218 | void calculate_outputm97(int); |
219 | void calculate_outputm98(int); |
220 | void calculate_outputm99(int); |
221 | void calculate_outputm100(int); |
222 | void calculate_outputm101(int); |
223 | void calculate_outputm102(int); |
224 | void calculate_outputm103(int); |
225 | void calculate_outputm104(int); |
226 | void calculate_outputm105(int); |
227 | void calculate_outputm106(int); |
228 | void calculate_outputm107(int); |
229 | void calculate_outputm108(int); |
230 | void calculate_outputm109(int); |
231 | void calculate_outputm110(int); |
232 | void calculate_outputm111(int); |
233 | void calculate_outputm112(int); |
234 | void calculate_outputm113(int); |
235 | void calculate_outputm114(int); |
236 | void calculate_outputm115(int); |
237 | void calculate_outputm116(int); |
238 | void calculate_outputm117(int); |
239 | void calculate_outputm118(int); |
240 | void calculate_outputm119(int); |
241 | void calculate_outputm120(int); |
242 | void calculate_outputm121(int); |
243 | void calculate_outputm122(int); |
244 | void calculate_outputm123(int); |
245 | void calculate_outputm124(int); |
246 | void calculate_outputm125(int); |
247 | void calculate_outputm126(int); |
248 | void calculate_outputm127(int); |
249 | void calculate_outputm128(int); |
250 | void calculate_outputm129(int); |
251 | void calculate_outputm130(int); |
252 | void calculate_outputm131(int); |
253 | void calculate_outputm132(int); |
254 | void calculate_outputm133(int); |
255 | void calculate_outputm134(int); |
256 | void calculate_outputm135(int); |
257 | void calculate_outputm136(int); |
258 | void calculate_outputm137(int); |
259 | void calculate_outputm138(int); |
260 | void calculate_outputm139(int); |
261 | void calculate_outputm140(int); |
262 | void calculate_outputm141(int); |
263 | void calculate_outputm142(int); |
264 | void calculate_outputm143(int); |
265 | void calculate_outputm144(int); |
266 | void calculate_outputm145(int); |
267 | void calculate_outputm146(int); |
268 | void calculate_outputm147(int); |
269 | void calculate_outputm148(int); |
270 | void calculate_outputm149(int); |
271 | void calculate_outputm150(int); |
272 | void calculate_outputm151(int); |
273 | void calculate_outputm152(int); |
274 | void calculate_outputm153(int); |
275 | void calculate_outputm154(int); |
276 | void calculate_outputm155(int); |
277 | void calculate_outputm156(int); |
278 | void calculate_outputm157(int); |
279 | |
280 | int a927814483 = 8; |
281 | int a1649592707 = 34; |
282 | int a231305105 = 13; |
283 | int a510889416 = 36; |
284 | int a1450658394 = 9; |
285 | int a1294378386 = 8; |
286 | int a938827910 = 33; |
287 | int a1136264456 = 35; |
288 | int a1551570219 = 32; |
289 | int a1583922005 = 6; |
290 | int a1591641889 = 11; |
291 | int a2077863541 = 14; |
292 | int a1384943560 = 34; |
293 | int a1944816302 = 32; |
294 | int a43901077 = 33; |
295 | int a1796618233 = 33; |
296 | int a1041640432 = 10; |
297 | int a1491567675 = 16; |
298 | int a469914660 = 14; |
299 | int a843079661 = 35; |
300 | int a1554992028 = 8; |
301 | int a1868984816 = 12; |
302 | int a1933271548 = 9; |
303 | int a1379546326 = 7; |
304 | int cf = 1; |
305 | int a181636438 = 33; |
306 | int a2108703896 = 36; |
307 | int a1669722568 = 32; |
308 | int a1431178715 = 32; |
309 | int a1580663338 = 33; |
310 | |
311 | |
312 | void errorCheck() { |
313 | if(((a1554992028 == 9 && a1933271548 == 3) && a1551570219 == 34)){ |
314 | cf = 0; |
315 | reach_error_0(); |
316 | } |
317 | if(((a1649592707 == 35 && a1933271548 == 5) && a1551570219 == 34)){ |
318 | cf = 0; |
319 | reach_error_1(); |
320 | } |
321 | if(((a469914660 == 8 && a1868984816 == 8) && a1551570219 == 36)){ |
322 | cf = 0; |
323 | reach_error_2(); |
324 | } |
325 | if(((a1554992028 == 12 && a1041640432 == 4) && a1551570219 == 32)){ |
326 | cf = 0; |
327 | reach_error_3(); |
328 | } |
329 | if(((a2077863541 == 11 && a1868984816 == 10) && a1551570219 == 36)){ |
330 | cf = 0; |
331 | reach_error_4(); |
332 | } |
333 | if(((a1591641889 == 9 && a1933271548 == 8) && a1551570219 == 34)){ |
334 | cf = 0; |
335 | reach_error_5(); |
336 | } |
337 | if(((a1384943560 == 33 && a1669722568 == 35) && a1551570219 == 33)){ |
338 | cf = 0; |
339 | reach_error_6(); |
340 | } |
341 | if(((a1554992028 == 15 && a1933271548 == 3) && a1551570219 == 34)){ |
342 | cf = 0; |
343 | reach_error_7(); |
344 | } |
345 | if(((a1554992028 == 11 && a1669722568 == 33) && a1551570219 == 33)){ |
346 | cf = 0; |
347 | reach_error_8(); |
348 | } |
349 | if(((a1944816302 == 35 && a43901077 == 33) && a1551570219 == 35)){ |
350 | cf = 0; |
351 | reach_error_9(); |
352 | } |
353 | if(((a1136264456 == 36 && a1041640432 == 5) && a1551570219 == 32)){ |
354 | cf = 0; |
355 | reach_error_10(); |
356 | } |
357 | if(((a1384943560 == 35 && a1669722568 == 35) && a1551570219 == 33)){ |
358 | cf = 0; |
359 | reach_error_11(); |
360 | } |
361 | if(((a1583922005 == 7 && a1669722568 == 32) && a1551570219 == 33)){ |
362 | cf = 0; |
363 | reach_error_12(); |
364 | } |
365 | if(((a1583922005 == 9 && a1669722568 == 32) && a1551570219 == 33)){ |
366 | cf = 0; |
367 | reach_error_13(); |
368 | } |
369 | if(((a469914660 == 7 && a1868984816 == 8) && a1551570219 == 36)){ |
370 | cf = 0; |
371 | reach_error_14(); |
372 | } |
373 | if(((a1136264456 == 35 && a1041640432 == 8) && a1551570219 == 32)){ |
374 | cf = 0; |
375 | reach_error_15(); |
376 | } |
377 | if(((a2077863541 == 14 && a1868984816 == 10) && a1551570219 == 36)){ |
378 | cf = 0; |
379 | reach_error_16(); |
380 | } |
381 | if(((a1583922005 == 12 && a1669722568 == 32) && a1551570219 == 33)){ |
382 | cf = 0; |
383 | reach_error_17(); |
384 | } |
385 | if(((a1591641889 == 5 && a1868984816 == 9) && a1551570219 == 36)){ |
386 | cf = 0; |
387 | reach_error_18(); |
388 | } |
389 | if(((a1583922005 == 11 && a1669722568 == 32) && a1551570219 == 33)){ |
390 | cf = 0; |
391 | reach_error_19(); |
392 | } |
393 | if(((a1591641889 == 6 && a1933271548 == 8) && a1551570219 == 34)){ |
394 | cf = 0; |
395 | reach_error_20(); |
396 | } |
397 | if(((a1431178715 == 32 && a1041640432 == 9) && a1551570219 == 32)){ |
398 | cf = 0; |
399 | reach_error_21(); |
400 | } |
401 | if(((a1933271548 == 3 && a1669722568 == 34) && a1551570219 == 33)){ |
402 | cf = 0; |
403 | reach_error_22(); |
404 | } |
405 | if(((a927814483 == 9 && a43901077 == 35) && a1551570219 == 35)){ |
406 | cf = 0; |
407 | reach_error_23(); |
408 | } |
409 | if(((a1384943560 == 34 && a1669722568 == 35) && a1551570219 == 33)){ |
410 | cf = 0; |
411 | reach_error_24(); |
412 | } |
413 | if(((a1583922005 == 5 && a1669722568 == 32) && a1551570219 == 33)){ |
414 | cf = 0; |
415 | reach_error_25(); |
416 | } |
417 | if(((a1554992028 == 13 && a1669722568 == 33) && a1551570219 == 33)){ |
418 | cf = 0; |
419 | reach_error_26(); |
420 | } |
421 | if(((a1136264456 == 32 && a1041640432 == 8) && a1551570219 == 32)){ |
422 | cf = 0; |
423 | reach_error_27(); |
424 | } |
425 | if(((a1944816302 == 35 && a1041640432 == 10) && a1551570219 == 32)){ |
426 | cf = 0; |
427 | reach_error_28(); |
428 | } |
429 | if(((a1591641889 == 8 && a1868984816 == 9) && a1551570219 == 36)){ |
430 | cf = 0; |
431 | reach_error_29(); |
432 | } |
433 | if(((a1554992028 == 10 && a1933271548 == 3) && a1551570219 == 34)){ |
434 | cf = 0; |
435 | reach_error_30(); |
436 | } |
437 | if(((a1450658394 == 9 && a1669722568 == 36) && a1551570219 == 33)){ |
438 | cf = 0; |
439 | reach_error_31(); |
440 | } |
441 | if(((a1933271548 == 4 && a1669722568 == 34) && a1551570219 == 33)){ |
442 | cf = 0; |
443 | reach_error_32(); |
444 | } |
445 | if(((a1933271548 == 8 && a1669722568 == 34) && a1551570219 == 33)){ |
446 | cf = 0; |
447 | reach_error_33(); |
448 | } |
449 | if(((a231305105 == 12 && a1868984816 == 15) && a1551570219 == 36)){ |
450 | cf = 0; |
451 | reach_error_34(); |
452 | } |
453 | if(((a1491567675 == 16 && a43901077 == 34) && a1551570219 == 35)){ |
454 | cf = 0; |
455 | reach_error_35(); |
456 | } |
457 | if(((a2077863541 == 13 && a1868984816 == 10) && a1551570219 == 36)){ |
458 | cf = 0; |
459 | reach_error_36(); |
460 | } |
461 | if(((a43901077 == 34 && a1041640432 == 7) && a1551570219 == 32)){ |
462 | cf = 0; |
463 | reach_error_37(); |
464 | } |
465 | if(((a1649592707 == 32 && a1041640432 == 11) && a1551570219 == 32)){ |
466 | cf = 0; |
467 | reach_error_38(); |
468 | } |
469 | if(((a1491567675 == 11 && a43901077 == 34) && a1551570219 == 35)){ |
470 | cf = 0; |
471 | reach_error_39(); |
472 | } |
473 | if(((a927814483 == 8 && a1933271548 == 9) && a1551570219 == 34)){ |
474 | cf = 0; |
475 | reach_error_40(); |
476 | } |
477 | if(((a1554992028 == 10 && a1041640432 == 4) && a1551570219 == 32)){ |
478 | cf = 0; |
479 | reach_error_41(); |
480 | } |
481 | if(((a927814483 == 13 && a1868984816 == 11) && a1551570219 == 36)){ |
482 | cf = 0; |
483 | reach_error_42(); |
484 | } |
485 | if(((a1554992028 == 12 && a1933271548 == 10) && a1551570219 == 34)){ |
486 | cf = 0; |
487 | reach_error_43(); |
488 | } |
489 | if(((a927814483 == 13 && a43901077 == 35) && a1551570219 == 35)){ |
490 | cf = 0; |
491 | reach_error_44(); |
492 | } |
493 | if(((a1944816302 == 33 && a1041640432 == 10) && a1551570219 == 32)){ |
494 | cf = 0; |
495 | reach_error_45(); |
496 | } |
497 | if(((a938827910 == 35 && a1868984816 == 12) && a1551570219 == 36)){ |
498 | cf = 0; |
499 | reach_error_46(); |
500 | } |
501 | if(((a1649592707 == 32 && a1933271548 == 5) && a1551570219 == 34)){ |
502 | cf = 0; |
503 | reach_error_47(); |
504 | } |
505 | if(((a1591641889 == 9 && a1868984816 == 9) && a1551570219 == 36)){ |
506 | cf = 0; |
507 | reach_error_48(); |
508 | } |
509 | if(((a1796618233 == 33 && a1868984816 == 13) && a1551570219 == 36)){ |
510 | cf = 0; |
511 | reach_error_49(); |
512 | } |
513 | if(((a1554992028 == 11 && a1041640432 == 4) && a1551570219 == 32)){ |
514 | cf = 0; |
515 | reach_error_50(); |
516 | } |
517 | if(((a1136264456 == 36 && a1041640432 == 8) && a1551570219 == 32)){ |
518 | cf = 0; |
519 | reach_error_51(); |
520 | } |
521 | if(((a1554992028 == 13 && a1933271548 == 10) && a1551570219 == 34)){ |
522 | cf = 0; |
523 | reach_error_52(); |
524 | } |
525 | if(((a43901077 == 35 && a1041640432 == 7) && a1551570219 == 32)){ |
526 | cf = 0; |
527 | reach_error_53(); |
528 | } |
529 | if(((a1649592707 == 35 && a1041640432 == 11) && a1551570219 == 32)){ |
530 | cf = 0; |
531 | reach_error_54(); |
532 | } |
533 | if(((a1491567675 == 12 && a43901077 == 34) && a1551570219 == 35)){ |
534 | cf = 0; |
535 | reach_error_55(); |
536 | } |
537 | if(((a1591641889 == 10 && a1933271548 == 8) && a1551570219 == 34)){ |
538 | cf = 0; |
539 | reach_error_56(); |
540 | } |
541 | if(((a927814483 == 11 && a1933271548 == 9) && a1551570219 == 34)){ |
542 | cf = 0; |
543 | reach_error_57(); |
544 | } |
545 | if(((a1933271548 == 9 && a1669722568 == 34) && a1551570219 == 33)){ |
546 | cf = 0; |
547 | reach_error_58(); |
548 | } |
549 | if(((a927814483 == 10 && a1933271548 == 9) && a1551570219 == 34)){ |
550 | cf = 0; |
551 | reach_error_59(); |
552 | } |
553 | if(((a1944816302 == 34 && a1041640432 == 10) && a1551570219 == 32)){ |
554 | cf = 0; |
555 | reach_error_60(); |
556 | } |
557 | if(((a1379546326 == 11 && a1041640432 == 6) && a1551570219 == 32)){ |
558 | cf = 0; |
559 | reach_error_61(); |
560 | } |
561 | if(((a2077863541 == 8 && a1868984816 == 10) && a1551570219 == 36)){ |
562 | cf = 0; |
563 | reach_error_62(); |
564 | } |
565 | if(((a938827910 == 34 && a1868984816 == 12) && a1551570219 == 36)){ |
566 | cf = 0; |
567 | reach_error_63(); |
568 | } |
569 | if(((a469914660 == 14 && a1868984816 == 8) && a1551570219 == 36)){ |
570 | cf = 0; |
571 | reach_error_64(); |
572 | } |
573 | if(((a2108703896 == 33 && a1933271548 == 4) && a1551570219 == 34)){ |
574 | cf = 0; |
575 | reach_error_65(); |
576 | } |
577 | if(((a843079661 == 33 && a43901077 == 36) && a1551570219 == 35)){ |
578 | cf = 0; |
579 | reach_error_66(); |
580 | } |
581 | if(((a1379546326 == 9 && a1041640432 == 6) && a1551570219 == 32)){ |
582 | cf = 0; |
583 | reach_error_67(); |
584 | } |
585 | if(((a927814483 == 12 && a1868984816 == 11) && a1551570219 == 36)){ |
586 | cf = 0; |
587 | reach_error_68(); |
588 | } |
589 | if(((a927814483 == 9 && a1933271548 == 9) && a1551570219 == 34)){ |
590 | cf = 0; |
591 | reach_error_69(); |
592 | } |
593 | if(((a1796618233 == 36 && a1868984816 == 13) && a1551570219 == 36)){ |
594 | cf = 0; |
595 | reach_error_70(); |
596 | } |
597 | if(((a1384943560 == 36 && a1669722568 == 35) && a1551570219 == 33)){ |
598 | cf = 0; |
599 | reach_error_71(); |
600 | } |
601 | if(((a1554992028 == 15 && a1041640432 == 4) && a1551570219 == 32)){ |
602 | cf = 0; |
603 | reach_error_72(); |
604 | } |
605 | if(((a1379546326 == 8 && a1041640432 == 6) && a1551570219 == 32)){ |
606 | cf = 0; |
607 | reach_error_73(); |
608 | } |
609 | if(((a1933271548 == 7 && a1669722568 == 34) && a1551570219 == 33)){ |
610 | cf = 0; |
611 | reach_error_74(); |
612 | } |
613 | if(((a231305105 == 13 && a1868984816 == 15) && a1551570219 == 36)){ |
614 | cf = 0; |
615 | reach_error_75(); |
616 | } |
617 | if(((a1591641889 == 11 && a1933271548 == 8) && a1551570219 == 34)){ |
618 | cf = 0; |
619 | reach_error_76(); |
620 | } |
621 | if(((a1384943560 == 32 && a1669722568 == 35) && a1551570219 == 33)){ |
622 | cf = 0; |
623 | reach_error_77(); |
624 | } |
625 | if(((a1554992028 == 8 && a1933271548 == 3) && a1551570219 == 34)){ |
626 | cf = 0; |
627 | reach_error_78(); |
628 | } |
629 | if(((a1554992028 == 9 && a1041640432 == 4) && a1551570219 == 32)){ |
630 | cf = 0; |
631 | reach_error_79(); |
632 | } |
633 | if(((a1591641889 == 7 && a1868984816 == 9) && a1551570219 == 36)){ |
634 | cf = 0; |
635 | reach_error_80(); |
636 | } |
637 | if(((a1554992028 == 11 && a1933271548 == 10) && a1551570219 == 34)){ |
638 | cf = 0; |
639 | reach_error_81(); |
640 | } |
641 | if(((a1591641889 == 6 && a1868984816 == 9) && a1551570219 == 36)){ |
642 | cf = 0; |
643 | reach_error_82(); |
644 | } |
645 | if(((a938827910 == 36 && a1868984816 == 12) && a1551570219 == 36)){ |
646 | cf = 0; |
647 | reach_error_83(); |
648 | } |
649 | if(((a1580663338 == 32 && a1868984816 == 14) && a1551570219 == 36)){ |
650 | cf = 0; |
651 | reach_error_84(); |
652 | } |
653 | if(((a1450658394 == 10 && a1669722568 == 36) && a1551570219 == 33)){ |
654 | cf = 0; |
655 | reach_error_85(); |
656 | } |
657 | if(((a938827910 == 33 && a1868984816 == 12) && a1551570219 == 36)){ |
658 | cf = 0; |
659 | reach_error_86(); |
660 | } |
661 | if(((a1554992028 == 10 && a1933271548 == 10) && a1551570219 == 34)){ |
662 | cf = 0; |
663 | reach_error_87(); |
664 | } |
665 | if(((a1933271548 == 5 && a1669722568 == 34) && a1551570219 == 33)){ |
666 | cf = 0; |
667 | reach_error_88(); |
668 | } |
669 | if(((a1294378386 == 8 && a43901077 == 32) && a1551570219 == 35)){ |
670 | cf = 0; |
671 | reach_error_89(); |
672 | } |
673 | if(((a1450658394 == 8 && a1669722568 == 36) && a1551570219 == 33)){ |
674 | cf = 0; |
675 | reach_error_90(); |
676 | } |
677 | if(((a231305105 == 9 && a1868984816 == 15) && a1551570219 == 36)){ |
678 | cf = 0; |
679 | reach_error_91(); |
680 | } |
681 | if(((a1554992028 == 8 && a1933271548 == 10) && a1551570219 == 34)){ |
682 | cf = 0; |
683 | reach_error_92(); |
684 | } |
685 | if(((a1944816302 == 34 && a43901077 == 33) && a1551570219 == 35)){ |
686 | cf = 0; |
687 | reach_error_93(); |
688 | } |
689 | if(((a1294378386 == 4 && a43901077 == 32) && a1551570219 == 35)){ |
690 | cf = 0; |
691 | reach_error_94(); |
692 | } |
693 | if(((a2108703896 == 34 && a1933271548 == 4) && a1551570219 == 34)){ |
694 | cf = 0; |
695 | reach_error_95(); |
696 | } |
697 | if(((a1796618233 == 32 && a1868984816 == 13) && a1551570219 == 36)){ |
698 | cf = 0; |
699 | reach_error_96(); |
700 | } |
701 | if(((a927814483 == 13 && a1933271548 == 9) && a1551570219 == 34)){ |
702 | cf = 0; |
703 | reach_error_97(); |
704 | } |
705 | if(((a1294378386 == 9 && a43901077 == 32) && a1551570219 == 35)){ |
706 | cf = 0; |
707 | reach_error_98(); |
708 | } |
709 | if(((a181636438 == 35 && a1933271548 == 7) && a1551570219 == 34)){ |
710 | cf = 0; |
711 | reach_error_99(); |
712 | } |
713 | } |
714 | void calculate_outputm37(int input) { |
715 | if(((((input == 5) && (a1551570219 == 33 && cf==1 )) && a1554992028 == 15) && a1669722568 == 33)) { |
716 | cf = 0; |
717 | a1868984816 = 10; |
718 | a1551570219 = 36 ; |
719 | a2077863541 = 10; |
720 | |
721 | } |
722 | if(((a1551570219 == 33 && (( cf==1 && a1669722568 == 33) && (input == 3))) && a1554992028 == 15)) { |
723 | cf = 0; |
724 | a1669722568 = 32 ; |
725 | a1583922005 = 10; |
726 | |
727 | } |
728 | if(((input == 1) && (a1554992028 == 15 && ((a1669722568 == 33 && cf==1 ) && a1551570219 == 33)))) { |
729 | cf = 0; |
730 | a1669722568 = 36 ; |
731 | a1450658394 = 12; |
732 | |
733 | } |
734 | } |
735 | void calculate_outputm1(int input) { |
736 | if(( cf==1 && a1554992028 == 15)) { |
737 | calculate_outputm37(input); |
738 | } |
739 | } |
740 | void calculate_outputm41(int input) { |
741 | if((a1669722568 == 32 && (a1583922005 == 10 && (( cf==1 && (input == 4)) && a1551570219 == 33)))) { |
742 | cf = 0; |
743 | a1551570219 = 32 ; |
744 | a1041640432 = 6; |
745 | a1379546326 = 8; |
746 | |
747 | } |
748 | if((a1669722568 == 32 && ((input == 1) && (a1551570219 == 33 && ( cf==1 && a1583922005 == 10))))) { |
749 | cf = 0; |
750 | a1669722568 = 33 ; |
751 | a1554992028 = 15; |
752 | |
753 | } |
754 | if((a1669722568 == 32 && ((( cf==1 && a1551570219 == 33) && a1583922005 == 10) && (input == 5)))) { |
755 | cf = 0; |
756 | |
757 | |
758 | } |
759 | } |
760 | void calculate_outputm2(int input) { |
761 | if((a1583922005 == 10 && cf==1 )) { |
762 | calculate_outputm41(input); |
763 | } |
764 | } |
765 | void calculate_outputm58(int input) { |
766 | if(((a1669722568 == 36 && ((input == 5) && (a1450658394 == 12 && cf==1 ))) && a1551570219 == 33)) { |
767 | cf = 0; |
768 | a1551570219 = 32 ; |
769 | a1136264456 = 32 ; |
770 | a1041640432 = 8; |
771 | |
772 | } |
773 | if(((input == 3) && ((a1450658394 == 12 && ( cf==1 && a1551570219 == 33)) && a1669722568 == 36))) { |
774 | cf = 0; |
775 | |
776 | |
777 | } |
778 | } |
779 | void calculate_outputm59(int input) { |
780 | if(((a1551570219 == 33 && (a1450658394 == 14 && ( cf==1 && (input == 1)))) && a1669722568 == 36)) { |
781 | cf = 0; |
782 | a510889416 = 32 ; |
783 | a1551570219 = 34 ; |
784 | a1933271548 = 6; |
785 | |
786 | } |
787 | if((((a1669722568 == 36 && (a1450658394 == 14 && cf==1 )) && a1551570219 == 33) && (input == 5))) { |
788 | cf = 0; |
789 | a1551570219 = 35 ; |
790 | a43901077 = 33 ; |
791 | a1944816302 = 32 ; |
792 | |
793 | } |
794 | } |
795 | void calculate_outputm5(int input) { |
796 | if((a1450658394 == 12 && cf==1 )) { |
797 | calculate_outputm58(input); |
798 | } |
799 | if(( cf==1 && a1450658394 == 14)) { |
800 | calculate_outputm59(input); |
801 | } |
802 | } |
803 | void calculate_outputm65(int input) { |
804 | if(((input == 5) && (a1136264456 == 33 && (( cf==1 && a1041640432 == 5) && a1551570219 == 32)))) { |
805 | cf = 0; |
806 | a43901077 = 33 ; |
807 | a1551570219 = 35 ; |
808 | a1944816302 = 32 ; |
809 | |
810 | } |
811 | if((a1136264456 == 33 && ((( cf==1 && (input == 1)) && a1041640432 == 5) && a1551570219 == 32))) { |
812 | cf = 0; |
813 | a1551570219 = 33 ; |
814 | a1669722568 = 36 ; |
815 | a1450658394 = 12; |
816 | |
817 | } |
818 | } |
819 | void calculate_outputm7(int input) { |
820 | if((a1136264456 == 33 && cf==1 )) { |
821 | calculate_outputm65(input); |
822 | } |
823 | } |
824 | void calculate_outputm69(int input) { |
825 | if((a1041640432 == 6 && (a1379546326 == 10 && ((a1551570219 == 32 && cf==1 ) && (input == 1))))) { |
826 | cf = 0; |
827 | a1551570219 = 35 ; |
828 | a43901077 = 35 ; |
829 | a927814483 = 9; |
830 | |
831 | } |
832 | if((a1379546326 == 10 && (((a1041640432 == 6 && cf==1 ) && (input == 3)) && a1551570219 == 32))) { |
833 | cf = 0; |
834 | a1431178715 = 34 ; |
835 | a1041640432 = 9; |
836 | |
837 | } |
838 | if(((a1551570219 == 32 && ((input == 5) && (a1041640432 == 6 && cf==1 ))) && a1379546326 == 10)) { |
839 | cf = 0; |
840 | |
841 | |
842 | } |
843 | } |
844 | void calculate_outputm71(int input) { |
845 | if(((((a1041640432 == 6 && cf==1 ) && a1551570219 == 32) && (input == 3)) && a1379546326 == 12)) { |
846 | cf = 0; |
847 | a1551570219 = 34 ; |
848 | a1933271548 = 10; |
849 | a1554992028 = 8; |
850 | |
851 | } |
852 | if((a1041640432 == 6 && (((a1379546326 == 12 && cf==1 ) && (input == 1)) && a1551570219 == 32))) { |
853 | cf = 0; |
854 | a43901077 = 32 ; |
855 | a1551570219 = 35 ; |
856 | a1294378386 = 10; |
857 | |
858 | } |
859 | if((((( cf==1 && (input == 5)) && a1379546326 == 12) && a1551570219 == 32) && a1041640432 == 6)) { |
860 | cf = 0; |
861 | a1379546326 = 10; |
862 | |
863 | } |
864 | } |
865 | void calculate_outputm8(int input) { |
866 | if(( cf==1 && a1379546326 == 10)) { |
867 | calculate_outputm69(input); |
868 | } |
869 | if((a1379546326 == 12 && cf==1 )) { |
870 | calculate_outputm71(input); |
871 | } |
872 | } |
873 | void calculate_outputm77(int input) { |
874 | if((((input == 4) && (a1551570219 == 32 && ( cf==1 && a1431178715 == 33))) && a1041640432 == 9)) { |
875 | cf = 0; |
876 | a1551570219 = 34 ; |
877 | a2108703896 = 33 ; |
878 | a1933271548 = 4; |
879 | |
880 | } |
881 | if((((( cf==1 && a1041640432 == 9) && (input == 3)) && a1431178715 == 33) && a1551570219 == 32)) { |
882 | cf = 0; |
883 | a1551570219 = 35 ; |
884 | a43901077 = 32 ; |
885 | a1294378386 = 11; |
886 | |
887 | } |
888 | } |
889 | void calculate_outputm79(int input) { |
890 | if(((input == 2) && (a1551570219 == 32 && (( cf==1 && a1041640432 == 9) && a1431178715 == 34)))) { |
891 | cf = 0; |
892 | a1551570219 = 33 ; |
893 | a1669722568 = 34 ; |
894 | a1933271548 = 9; |
895 | |
896 | } |
897 | if((a1431178715 == 34 && (a1551570219 == 32 && ((input == 3) && ( cf==1 && a1041640432 == 9))))) { |
898 | cf = 0; |
899 | a1649592707 = 34 ; |
900 | a1041640432 = 11; |
901 | |
902 | } |
903 | if((a1551570219 == 32 && ((input == 1) && (a1431178715 == 34 && ( cf==1 && a1041640432 == 9))))) { |
904 | cf = 0; |
905 | |
906 | |
907 | } |
908 | if((((( cf==1 && a1431178715 == 34) && a1551570219 == 32) && (input == 5)) && a1041640432 == 9)) { |
909 | cf = 0; |
910 | |
911 | |
912 | } |
913 | } |
914 | void calculate_outputm11(int input) { |
915 | if((a1431178715 == 33 && cf==1 )) { |
916 | calculate_outputm77(input); |
917 | } |
918 | if((a1431178715 == 34 && cf==1 )) { |
919 | calculate_outputm79(input); |
920 | } |
921 | } |
922 | void calculate_outputm81(int input) { |
923 | if((((( cf==1 && a1944816302 == 32) && a1551570219 == 32) && (input == 5)) && a1041640432 == 10)) { |
924 | cf = 0; |
925 | a1431178715 = 33 ; |
926 | a1041640432 = 9; |
927 | |
928 | } |
929 | if((((input == 1) && (( cf==1 && a1944816302 == 32) && a1041640432 == 10)) && a1551570219 == 32)) { |
930 | cf = 0; |
931 | a1551570219 = 36 ; |
932 | a1868984816 = 8; |
933 | a469914660 = 12; |
934 | |
935 | } |
936 | if(((a1551570219 == 32 && (( cf==1 && a1944816302 == 32) && (input == 2))) && a1041640432 == 10)) { |
937 | cf = 0; |
938 | a1551570219 = 35 ; |
939 | a43901077 = 32 ; |
940 | a1294378386 = 10; |
941 | |
942 | } |
943 | } |
944 | void calculate_outputm12(int input) { |
945 | if((a1944816302 == 32 && cf==1 )) { |
946 | calculate_outputm81(input); |
947 | } |
948 | } |
949 | void calculate_outputm85(int input) { |
950 | if((a1041640432 == 11 && ((a1649592707 == 34 && ( cf==1 && (input == 5))) && a1551570219 == 32))) { |
951 | cf = 0; |
952 | a1431178715 = 34 ; |
953 | a1041640432 = 9; |
954 | |
955 | } |
956 | if((((a1649592707 == 34 && (a1041640432 == 11 && cf==1 )) && (input == 2)) && a1551570219 == 32)) { |
957 | cf = 0; |
958 | a1551570219 = 36 ; |
959 | a1868984816 = 9; |
960 | a1591641889 = 5; |
961 | |
962 | } |
963 | if(((a1041640432 == 11 && (a1649592707 == 34 && ((input == 1) && cf==1 ))) && a1551570219 == 32)) { |
964 | cf = 0; |
965 | |
966 | |
967 | } |
968 | } |
969 | void calculate_outputm13(int input) { |
970 | if(( cf==1 && a1649592707 == 34)) { |
971 | calculate_outputm85(input); |
972 | } |
973 | } |
974 | void calculate_outputm95(int input) { |
975 | if(((a1649592707 == 36 && (((input == 3) && cf==1 ) && a1551570219 == 34)) && a1933271548 == 5)) { |
976 | cf = 0; |
977 | a1136264456 = 33 ; |
978 | a1551570219 = 32 ; |
979 | a1041640432 = 5; |
980 | |
981 | } |
982 | if((a1933271548 == 5 && (a1649592707 == 36 && ((input == 5) && (a1551570219 == 34 && cf==1 ))))) { |
983 | cf = 0; |
984 | a1551570219 = 35 ; |
985 | a43901077 = 33 ; |
986 | a1944816302 = 32 ; |
987 | |
988 | } |
989 | if((((a1649592707 == 36 && (a1551570219 == 34 && cf==1 )) && (input == 4)) && a1933271548 == 5)) { |
990 | cf = 0; |
991 | a1649592707 = 32 ; |
992 | a1551570219 = 32 ; |
993 | a1041640432 = 11; |
994 | |
995 | } |
996 | if((((( cf==1 && a1551570219 == 34) && a1933271548 == 5) && a1649592707 == 36) && (input == 1))) { |
997 | cf = 0; |
998 | a1551570219 = 33 ; |
999 | a1669722568 = 36 ; |
1000 | a1450658394 = 14; |
1001 | |
1002 | } |
1003 | } |
1004 | void calculate_outputm16(int input) { |
1005 | if(( cf==1 && a1649592707 == 36)) { |
1006 | calculate_outputm95(input); |
1007 | } |
1008 | } |
1009 | void calculate_outputm96(int input) { |
1010 | if(((((a510889416 == 33 && cf==1 ) && (input == 5)) && a1933271548 == 6) && a1551570219 == 34)) { |
1011 | cf = 0; |
1012 | a1669722568 = 36 ; |
1013 | a1551570219 = 33 ; |
1014 | a1450658394 = 12; |
1015 | |
1016 | } |
1017 | if((a1551570219 == 34 && ((a1933271548 == 6 && ((input == 1) && cf==1 )) && a510889416 == 33))) { |
1018 | cf = 0; |
1019 | |
1020 | |
1021 | } |
1022 | if((((a510889416 == 33 && ((input == 3) && cf==1 )) && a1933271548 == 6) && a1551570219 == 34)) { |
1023 | cf = 0; |
1024 | a1551570219 = 36 ; |
1025 | a1868984816 = 8; |
1026 | a469914660 = 12; |
1027 | |
1028 | } |
1029 | } |
1030 | void calculate_outputm97(int input) { |
1031 | if((a1933271548 == 6 && ((input == 3) && (( cf==1 && a510889416 == 32) && a1551570219 == 34)))) { |
1032 | cf = 0; |
1033 | a1649592707 = 36 ; |
1034 | a1933271548 = 5; |
1035 | |
1036 | } |
1037 | if(((((a1933271548 == 6 && cf==1 ) && a1551570219 == 34) && a510889416 == 32) && (input == 1))) { |
1038 | cf = 0; |
1039 | a1669722568 = 36 ; |
1040 | a1551570219 = 33 ; |
1041 | a1450658394 = 14; |
1042 | |
1043 | } |
1044 | if((a1551570219 == 34 && ((a1933271548 == 6 && ((input == 5) && cf==1 )) && a510889416 == 32))) { |
1045 | cf = 0; |
1046 | a1551570219 = 35 ; |
1047 | a43901077 = 33 ; |
1048 | a1944816302 = 32 ; |
1049 | |
1050 | } |
1051 | } |
1052 | void calculate_outputm17(int input) { |
1053 | if((a510889416 == 33 && cf==1 )) { |
1054 | calculate_outputm96(input); |
1055 | } |
1056 | if((a510889416 == 32 && cf==1 )) { |
1057 | calculate_outputm97(input); |
1058 | } |
1059 | } |
1060 | void calculate_outputm113(int input) { |
1061 | if((a43901077 == 33 && (a1551570219 == 35 && ((input == 1) && (a1944816302 == 32 && cf==1 ))))) { |
1062 | cf = 0; |
1063 | |
1064 | |
1065 | } |
1066 | if(((a1551570219 == 35 && (((input == 4) && cf==1 ) && a1944816302 == 32)) && a43901077 == 33)) { |
1067 | cf = 0; |
1068 | a1551570219 = 33 ; |
1069 | a1669722568 = 34 ; |
1070 | a1933271548 = 5; |
1071 | |
1072 | } |
1073 | if(((a1551570219 == 35 && (( cf==1 && a43901077 == 33) && (input == 5))) && a1944816302 == 32)) { |
1074 | cf = 0; |
1075 | a1551570219 = 34 ; |
1076 | a1649592707 = 36 ; |
1077 | a1933271548 = 5; |
1078 | |
1079 | } |
1080 | } |
1081 | void calculate_outputm22(int input) { |
1082 | if(( cf==1 && a1944816302 == 32)) { |
1083 | calculate_outputm113(input); |
1084 | } |
1085 | } |
1086 | void calculate_outputm119(int input) { |
1087 | if((((( cf==1 && a43901077 == 32) && a1294378386 == 10) && (input == 5)) && a1551570219 == 35)) { |
1088 | cf = 0; |
1089 | a1431178715 = 34 ; |
1090 | a1551570219 = 32 ; |
1091 | a1041640432 = 9; |
1092 | |
1093 | } |
1094 | if((((a1294378386 == 10 && ( cf==1 && a1551570219 == 35)) && (input == 3)) && a43901077 == 32)) { |
1095 | cf = 0; |
1096 | a1041640432 = 6; |
1097 | a1551570219 = 32 ; |
1098 | a1379546326 = 12; |
1099 | |
1100 | } |
1101 | if((((a1294378386 == 10 && (a43901077 == 32 && cf==1 )) && (input == 2)) && a1551570219 == 35)) { |
1102 | cf = 0; |
1103 | a1669722568 = 35 ; |
1104 | a1551570219 = 33 ; |
1105 | a1384943560 = 33 ; |
1106 | |
1107 | } |
1108 | } |
1109 | void calculate_outputm120(int input) { |
1110 | if((((a1294378386 == 11 && ( cf==1 && a43901077 == 32)) && (input == 3)) && a1551570219 == 35)) { |
1111 | cf = 0; |
1112 | a1868984816 = 10; |
1113 | a1551570219 = 36 ; |
1114 | a2077863541 = 11; |
1115 | |
1116 | } |
1117 | if((a1551570219 == 35 && (a1294378386 == 11 && (a43901077 == 32 && ( cf==1 && (input == 5)))))) { |
1118 | cf = 0; |
1119 | a1669722568 = 32 ; |
1120 | a1551570219 = 33 ; |
1121 | a1583922005 = 10; |
1122 | |
1123 | } |
1124 | if((a1294378386 == 11 && ((a1551570219 == 35 && (a43901077 == 32 && cf==1 )) && (input == 1)))) { |
1125 | cf = 0; |
1126 | a1551570219 = 36 ; |
1127 | a1796618233 = 34 ; |
1128 | a1868984816 = 13; |
1129 | |
1130 | } |
1131 | } |
1132 | void calculate_outputm23(int input) { |
1133 | if(( cf==1 && a1294378386 == 10)) { |
1134 | calculate_outputm119(input); |
1135 | } |
1136 | if(( cf==1 && a1294378386 == 11)) { |
1137 | calculate_outputm120(input); |
1138 | } |
1139 | } |
1140 | void calculate_outputm129(int input) { |
1141 | if(((a1868984816 == 8 && (( cf==1 && a469914660 == 12) && a1551570219 == 36)) && (input == 5))) { |
1142 | cf = 0; |
1143 | a1868984816 = 9; |
1144 | a1591641889 = 4; |
1145 | |
1146 | } |
1147 | if((((( cf==1 && (input == 4)) && a469914660 == 12) && a1868984816 == 8) && a1551570219 == 36)) { |
1148 | cf = 0; |
1149 | a469914660 = 14; |
1150 | |
1151 | } |
1152 | if(((a1868984816 == 8 && ((input == 3) && (a1551570219 == 36 && cf==1 ))) && a469914660 == 12)) { |
1153 | cf = 0; |
1154 | a1551570219 = 35 ; |
1155 | a43901077 = 33 ; |
1156 | a1944816302 = 32 ; |
1157 | |
1158 | } |
1159 | if((((a1868984816 == 8 && (a469914660 == 12 && cf==1 )) && (input == 1)) && a1551570219 == 36)) { |
1160 | cf = 0; |
1161 | a1669722568 = 36 ; |
1162 | a1551570219 = 33 ; |
1163 | a1450658394 = 12; |
1164 | |
1165 | } |
1166 | } |
1167 | void calculate_outputm27(int input) { |
1168 | if((a469914660 == 12 && cf==1 )) { |
1169 | calculate_outputm129(input); |
1170 | } |
1171 | } |
1172 | void calculate_outputm131(int input) { |
1173 | if(((input == 2) && (a1868984816 == 9 && (( cf==1 && a1551570219 == 36) && a1591641889 == 4)))) { |
1174 | cf = 0; |
1175 | a1669722568 = 36 ; |
1176 | a1551570219 = 33 ; |
1177 | a1450658394 = 9; |
1178 | |
1179 | } |
1180 | if((a1551570219 == 36 && ((( cf==1 && a1868984816 == 9) && a1591641889 == 4) && (input == 5)))) { |
1181 | cf = 0; |
1182 | a1868984816 = 11; |
1183 | a927814483 = 14; |
1184 | |
1185 | } |
1186 | if((((( cf==1 && (input == 1)) && a1551570219 == 36) && a1868984816 == 9) && a1591641889 == 4)) { |
1187 | cf = 0; |
1188 | a510889416 = 33 ; |
1189 | a1551570219 = 34 ; |
1190 | a1933271548 = 6; |
1191 | |
1192 | } |
1193 | } |
1194 | void calculate_outputm137(int input) { |
1195 | if(((input == 1) && ((( cf==1 && a1868984816 == 9) && a1591641889 == 11) && a1551570219 == 36))) { |
1196 | cf = 0; |
1197 | a1551570219 = 35 ; |
1198 | a43901077 = 33 ; |
1199 | a1944816302 = 32 ; |
1200 | |
1201 | } |
1202 | if((a1868984816 == 9 && ((a1591641889 == 11 && ( cf==1 && (input == 3))) && a1551570219 == 36))) { |
1203 | cf = 0; |
1204 | |
1205 | |
1206 | } |
1207 | if((a1868984816 == 9 && ((a1591641889 == 11 && (a1551570219 == 36 && cf==1 )) && (input == 5)))) { |
1208 | cf = 0; |
1209 | a1796618233 = 34 ; |
1210 | a1868984816 = 13; |
1211 | |
1212 | } |
1213 | } |
1214 | void calculate_outputm28(int input) { |
1215 | if((a1591641889 == 4 && cf==1 )) { |
1216 | calculate_outputm131(input); |
1217 | } |
1218 | if(( cf==1 && a1591641889 == 11)) { |
1219 | calculate_outputm137(input); |
1220 | } |
1221 | } |
1222 | void calculate_outputm139(int input) { |
1223 | if((((( cf==1 && (input == 1)) && a1868984816 == 10) && a2077863541 == 10) && a1551570219 == 36)) { |
1224 | cf = 0; |
1225 | a1551570219 = 33 ; |
1226 | a1669722568 = 32 ; |
1227 | a1583922005 = 10; |
1228 | |
1229 | } |
1230 | if((((input == 3) && (a2077863541 == 10 && ( cf==1 && a1551570219 == 36))) && a1868984816 == 10)) { |
1231 | cf = 0; |
1232 | a43901077 = 32 ; |
1233 | a1551570219 = 35 ; |
1234 | a1294378386 = 11; |
1235 | |
1236 | } |
1237 | } |
1238 | void calculate_outputm29(int input) { |
1239 | if((a2077863541 == 10 && cf==1 )) { |
1240 | calculate_outputm139(input); |
1241 | } |
1242 | } |
1243 | void calculate_outputm145(int input) { |
1244 | if((a1868984816 == 11 && (a1551570219 == 36 && (((input == 3) && cf==1 ) && a927814483 == 14)))) { |
1245 | cf = 0; |
1246 | a1868984816 = 9; |
1247 | a1591641889 = 4; |
1248 | |
1249 | } |
1250 | } |
1251 | void calculate_outputm30(int input) { |
1252 | if((a927814483 == 14 && cf==1 )) { |
1253 | calculate_outputm145(input); |
1254 | } |
1255 | } |
1256 | void calculate_outputm152(int input) { |
1257 | if((a1868984816 == 13 && (((input == 5) && (a1796618233 == 34 && cf==1 )) && a1551570219 == 36))) { |
1258 | cf = 0; |
1259 | a1551570219 = 35 ; |
1260 | a43901077 = 33 ; |
1261 | a1944816302 = 32 ; |
1262 | |
1263 | } |
1264 | if((a1551570219 == 36 && ((input == 2) && (a1796618233 == 34 && ( cf==1 && a1868984816 == 13))))) { |
1265 | cf = 0; |
1266 | a1933271548 = 9; |
1267 | a1551570219 = 34 ; |
1268 | a927814483 = 9; |
1269 | |
1270 | } |
1271 | if(((input == 1) && (((a1551570219 == 36 && cf==1 ) && a1796618233 == 34) && a1868984816 == 13))) { |
1272 | cf = 0; |
1273 | a1868984816 = 9; |
1274 | a1591641889 = 11; |
1275 | |
1276 | } |
1277 | } |
1278 | void calculate_outputm32(int input) { |
1279 | if(( cf==1 && a1796618233 == 34)) { |
1280 | calculate_outputm152(input); |
1281 | } |
1282 | } |
1283 | |
1284 | void calculate_output(int input) { |
1285 | cf = 1; |
1286 | |
1287 | if(( cf==1 && a1551570219 == 33)) { |
1288 | if((a1669722568 == 33 && cf==1 )) { |
1289 | calculate_outputm1(input); |
1290 | } |
1291 | if((a1669722568 == 32 && cf==1 )) { |
1292 | calculate_outputm2(input); |
1293 | } |
1294 | if((a1669722568 == 36 && cf==1 )) { |
1295 | calculate_outputm5(input); |
1296 | } |
1297 | } |
1298 | if(( cf==1 && a1551570219 == 32)) { |
1299 | if((a1041640432 == 5 && cf==1 )) { |
1300 | calculate_outputm7(input); |
1301 | } |
1302 | if((a1041640432 == 6 && cf==1 )) { |
1303 | calculate_outputm8(input); |
1304 | } |
1305 | if(( cf==1 && a1041640432 == 9)) { |
1306 | calculate_outputm11(input); |
1307 | } |
1308 | if((a1041640432 == 10 && cf==1 )) { |
1309 | calculate_outputm12(input); |
1310 | } |
1311 | if((a1041640432 == 11 && cf==1 )) { |
1312 | calculate_outputm13(input); |
1313 | } |
1314 | } |
1315 | if(( cf==1 && a1551570219 == 34)) { |
1316 | if(( cf==1 && a1933271548 == 5)) { |
1317 | calculate_outputm16(input); |
1318 | } |
1319 | if((a1933271548 == 6 && cf==1 )) { |
1320 | calculate_outputm17(input); |
1321 | } |
1322 | } |
1323 | if(( cf==1 && a1551570219 == 35)) { |
1324 | if(( cf==1 && a43901077 == 33)) { |
1325 | calculate_outputm22(input); |
1326 | } |
1327 | if((a43901077 == 32 && cf==1 )) { |
1328 | calculate_outputm23(input); |
1329 | } |
1330 | } |
1331 | if(( cf==1 && a1551570219 == 36)) { |
1332 | if((a1868984816 == 8 && cf==1 )) { |
1333 | calculate_outputm27(input); |
1334 | } |
1335 | if(( cf==1 && a1868984816 == 9)) { |
1336 | calculate_outputm28(input); |
1337 | } |
1338 | if(( cf==1 && a1868984816 == 10)) { |
1339 | calculate_outputm29(input); |
1340 | } |
1341 | if(( cf==1 && a1868984816 == 11)) { |
1342 | calculate_outputm30(input); |
1343 | } |
1344 | if((a1868984816 == 13 && cf==1 )) { |
1345 | calculate_outputm32(input); |
1346 | } |
1347 | } |
1348 | errorCheck(); |
1349 | } |
1350 | |
1351 | int main() |
1352 | { |
1353 | // main i/o-loop |
1354 | while(1) |
1355 | { |
1356 | // read input |
1357 | int input; |
1358 | input = __VERIFIER_nondet_int(); |
1359 | // operate eca engine |
1360 | if((input != 5) && (input != 1) && (input != 3) && (input != 2) && (input != 4)) |
1361 | return -2; |
1362 | calculate_output(input); |
1363 | } |
1364 | } |
| Date | Time | Level | Component | Message |
|---|---|---|---|---|
| 2024-12-13 | 09:57:22:141 | INFO | CPAMain.detectFrontendLanguageIfNecessary | Language C detected and set for analysis |
| 2024-12-13 | 09:57:22:165 | INFO | ResourceLimitChecker.fromConfiguration | Using the following resource limits: CPU-time limit of 900s |
| 2024-12-13 | 09:57:22:283 | INFO | CPAchecker.run | CPAchecker 3.1-svn-96157deb60+ / predicateAnalysis (OpenJDK 64-Bit Server VM 17.0.13) started |
| 2024-12-13 | 09:57:22:302 | INFO | CPAchecker.parse | Parsing CFA from file(s) "../sv-benchmarks/c/eca-rers2018/Problem10.c" |
| 2024-12-13 | 09:57:24:334 | INFO | PredicateCPA PredicateCPA.<init> | Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant) and JFactory 1.21. |
| 2024-12-13 | 09:57:24:607 | INFO | PredicateCPA PredicateCPARefiner.<init> | Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy. |
| 2024-12-13 | 09:57:24:655 | INFO | CPAchecker.runAlgorithm | Starting analysis ... |
| 2024-12-13 | 09:57:24:657 | INFO | FindErrorCondition.run | Finding error condition... |
| 2024-12-13 | 10:12:08:428 | WARNING | ForceTerminationOnShutdown$1.shutdownRequested | Shutdown requested (The CPU-time limit of 900s has elapsed.), waiting for termination. |
| 2024-12-13 | 10:12:08:463 | WARNING | ShutdownNotifier.shutdownIfNecessary | Warning: Analysis interrupted (The CPU-time limit of 900s has elapsed.) |
| Statistics Name | Statistics Value | Additional Value |
|---|---|---|
| PredicateCPA statistics | ||
| Number of abstractions | 407 | 2% of all post computations |
| Times abstraction was reused | 0 | |
| Because of function entry/exit | 0 | 0% |
| Because of loop head | 12 | 3% |
| Because of join nodes | 0 | 0% |
| Because of threshold | 0 | 0% |
| Because of target state | 395 | 97% |
| Times precision was empty | 2 | 0% |
| Times precision was {false} | 0 | 0% |
| Times result was cached | 0 | 0% |
| Times cartesian abs was used | 0 | 0% |
| Times boolean abs was used | 405 | 100% |
| Times result was 'false' | 386 | 95% |
| Number of strengthen sat checks | 0 | |
| Number of coverage checks | 11642 | |
| BDD entailment checks | 6 | |
| Number of SMT sat checks | 0 | |
| trivial | 0 | |
| cached | 0 | |
| Max ABE block size | 981 | |
| Avg ABE block size | 787.04 | sum: 320325, count: 407, min: 31, max: 981 |
| Number of predicates discovered | 37 | |
| Number of abstraction locations | 2 | |
| Max number of predicates per location | 36 | |
| Avg number of predicates per location | 21 | |
| Total predicates per abstraction | 2591 | |
| Max number of predicates per abstraction | 36 | |
| Avg number of predicates per abstraction | 6.40 | |
| Number of irrelevant predicates | 390 | 15% |
| Number of preds handled by boolean abs | 2201 | 85% |
| Total number of models for allsat | 28 | |
| Max number of models for allsat | 4 | |
| Avg number of models for allsat | 0.07 | |
| Time for post operator | 0.329s | |
| Time for path formula creation | 0.316s | |
| Time for strengthen operator | 0.022s | |
| Time for prec operator | 38.157s | |
| Time for abstraction | 38.122s | Max: 0.177s, Count: 407 |
| Boolean abstraction | 32.387s | |
| Solving time | 32.150s | Max: 0.122s |
| Model enumeration time | 0.187s | |
| Time for BDD construction | 0.010s | Max: 0.003s |
| Time for merge operator | 0.056s | |
| Time for coverage checks | 0.001s | |
| Time for BDD entailment checks | 0.000s | |
| Total time for SMT solver (w/o itp) | 32.337s | |
| Number of path formula cache hits | 22273 | 83% |
| Inside post operator | ||
| Inside path formula creation | ||
| Time for path formula computation | 0.293s | |
| Total number of created targets for pointer analysis | 0 | |
| Number of BDD nodes | 3453 | |
| Size of BDD node table | 62921 | |
| Size of BDD cache | 6299 | |
| Size of BDD node cleanup queue | 0.63 | sum: 1949, count: 3108, min: 0, max: 444 |
| Time for BDD node cleanup | 0.005s | |
| Time for BDD garbage collection | 0.000s | in 0 runs |
| KeyValue statistics | ||
| Init. function predicates | 0 | |
| Init. global predicates | 0 | |
| Init. location predicates | 0 | |
| Invariant Generation statistics | ||
| AutomatonAnalysis (SVCOMP) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.089s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 21454, count: 21454, min: 1, max: 1 [1 x 21454] |
| Number of states with assumption transitions | 0 | |
| Code Coverage | ||
| Function coverage | 1.000 | |
| Visited lines | 805 | |
| Total lines | 808 | |
| Line coverage | 0.996 | |
| Visited conditions | 1440 | |
| Total conditions | 1440 | |
| Condition coverage | 1.000 | |
| CPAchecker general statistics | ||
| Number of program locations | 2279 | |
| Number of CFA edges (per node) | 2690 | count: 2279, min: 0, max: 2, avg: 1.18 |
| Number of relevant variables | 73 | |
| Number of functions | 146 | |
| Number of loops (and loop nodes) | 1 | sum: 10, min: 10, max: 10, avg: 10.00 |
| Size of reached set | 2495 | |
| Number of reached locations | 1474 | 65% |
| Avg states per location | 1 | |
| Max states per location | 91 | at node N13 |
| Number of reached functions | 146 | 100% |
| Number of partitions | 2494 | |
| Avg size of partitions | 1 | |
| Max size of partitions | 2 | with key [N1928 before line 1354, Function main called from node N1926, stack depth 1 [3f362135], stack [main]] |
| Number of target states | 1 | |
| Size of final wait list | 4 | |
| Time for analysis setup | 2.352s | |
| Time for loading CPAs | 0.864s | |
| Time for loading parser | 0.180s | |
| Time for CFA construction | 1.096s | |
| Time for parsing file(s) | 0.282s | |
| Time for AST to CFA | 0.446s | |
| Time for CFA sanity check | 0.055s | |
| Time for post-processing | 0.253s | |
| Time for loop structure | 0.012s | |
| Time for AST structure | 0.000s | |
| Time for CFA export | 1.305s | |
| Time for function pointers resolving | 0.008s | |
| Function calls via function pointers | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Instrumented function pointer calls | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Function calls with function pointer arguments | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Instrumented function pointer arguments | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Time for classifying variables | 0.156s | |
| Time for collecting variables | 0.086s | |
| Time for solving dependencies | 0.001s | |
| Time for building hierarchy | 0.000s | |
| Time for building classification | 0.056s | |
| Time for exporting data | 0.013s | |
| Time for Analysis | 883.805s | |
| CPU time for analysis | 893.000s | |
| Total time for CPAchecker | 886.161s | |
| Total CPU time for CPAchecker | 900.250s | |
| Time for statistics | 0.148s | |
| Time for Garbage Collector | 0.165s | in 32 runs |
| Garbage Collector(s) used | G1 Old Generation, G1 Young Generation | |
| Used heap memory | 70MB ( 67 MiB) max; 59MB ( 56 MiB) avg; 88MB ( 84 MiB) peak | |
| Used non-heap memory | 63MB ( 60 MiB) max; 60MB ( 57 MiB) avg; 64MB ( 61 MiB) peak | |
| Used in G1 Old Gen pool | 27MB ( 25 MiB) max; 27MB ( 25 MiB) avg; 27MB ( 25 MiB) peak | |
| Allocated heap memory | 1056MB ( 1008 MiB) max; 85MB ( 81 MiB) avg | |
| Allocated non-heap memory | 64MB ( 61 MiB) max; 64MB ( 61 MiB) avg | |
| Total process virtual memory | 7694MB ( 7337 MiB) max; 7680MB ( 7324 MiB) avg |
| # | Configuration Name | Configuration Value |
|---|---|---|
| 1 | analysis.algorithm.CEGAR | true |
| 2 | analysis.algorithm.findErrorCondition | true |
| 3 | analysis.name | predicateAnalysis |
| 4 | analysis.programNames | ../sv-benchmarks/c/eca-rers2018/Problem10.c |
| 5 | analysis.traversal.order | bfs |
| 6 | analysis.traversal.useCallstack | true |
| 7 | analysis.traversal.useReversePostorder | true |
| 8 | ARGCPA.cpa | cpa.composite.CompositeCPA |
| 9 | cegar.refiner | cpa.predicate.PredicateRefiner |
| 10 | CompositeCPA.cpas | cpa.location.LocationCPA, cpa.callstack.CallstackCPA, cpa.functionpointer.FunctionPointerCPA, cpa.predicate.PredicateCPA, $specification |
| 11 | cpa | cpa.arg.ARGCPA |
| 12 | cpa.composite.aggregateBasicBlocks | true |
| 13 | cpa.predicate.blk.alwaysAtFunctions | false |
| 14 | cpa.predicate.blk.alwaysAtLoops | true |
| 15 | cpa.predicate.memoryAllocationsAlwaysSucceed | true |
| 16 | cpa.predicate.refinement.performInitialStaticRefinement | true |
| 17 | language | C |
| 18 | limits.time.cpu | 900s |
| 19 | log.level | INFO |
| 20 | overflow.config | predicateAnalysis--overflow.properties |
| 21 | specification | config/specification/sv-comp-reachability.spc |
This table was generated by CPAchecker. For feedback, questions, and bug reports please use our issue tracker.
License: Apache 2.0 License
Source: {{dependency.repository}}
{{dependency.copyright}}
License:
Full text of license
{{dependencies.licenses[dependency.licenseId]}}